Tagging @fdedden and @RyanGlScott so that they take a look.

Good catch! Here is a concrete test case that demonstrates the bug in action:

{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Language.Copilot

spec :: Spec
spec = do
  let s :: Stream Bool
      s = drop 2 ([False, False] ++ true)
  trigger "example" s [arg s]

main :: IO ()
main = interpret 5 spec

Intuitively, I would expect drop 2 ([False, False] ++ true) to be equivalent to true, but in practice, Copilot rejects this with an error:

$ runghc Bug.hs
Bug.hs: Copilot error: Drop index overflow!
CallStack (from HasCallStack):
  error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.3-inplace:Copilot.Language.Error

On the other hand, drop 1 ([False, False] ++ true) does not throw an error. As such, I think your suggested fix of using k > length xs is apt.

(It would be helpful to include something like the program above as a test case.)

Good catch! Here is a concrete test case that demonstrates the bug in action:

{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Language.Copilot

spec :: Spec
spec = do
  let s :: Stream Bool
      s = drop 2 ([False, False] ++ true)
  trigger "example" s [arg s]

main :: IO ()
main = interpret 5 spec

Intuitively, I would expect drop 2 ([False, False] ++ true) to be equivalent to true, but in practice, Copilot rejects this with an error:

$ runghc Bug.hs
Bug.hs: Copilot error: Drop index overflow!
CallStack (from HasCallStack):
  error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.3-inplace:Copilot.Language.Error

On the other hand, drop 1 ([False, False] ++ true) does not throw an error. As such, I think your suggested fix of using k > length xs is apt.

(It would be helpful to include something like the program above as a test case.)

Thanks for the review!
Could you recommend a module to add such tests? I'm not very familiar with the Copilot source tree yet.

Could you recommend a module to add such tests?

Since the property of interest is checked in copilot-language, I think it makes sense to add a regression test in the copilot-language test suite. Currently, the copilot-language test suite only contains property-based tests (via QuickCheck), however. We could imagine adding some additional machinery to support a unit test that checks to see if reifying drop 2 [False, False] ++ true throws an exception or not, similar to this unit test in copilot-theorem.

This would take a fair bit of extra work, however, so I'll defer to @ivanperez-keera on whether we want to do all of this as part of this PR.

Thinking about this some more, I think that changing k >= length xs to k > length xs in Copilot.Language.Analyze is not necessary, and that we should instead make it the sole responsibility of the drop function to ensure that we drop the expected number of elements. To justify this, let me make a handful of claims:

Claim 1: There is an invariant that Drop is always applied to Append

When I say "Drop" and "Append" here, I mean in the sense of the data constructors for Stream in copilot-language, not the user-facing drop or (++) functions. The reason I claim that this invariant exists is because of how Drop is reified:

Note that reifying Drop k e1 will only succeed if e1 is an Append value. This invariant is not documented in the definition of Stream (perhaps it should be), but it is there all the same. This means that if you manually construct a Drop value (i.e., by directly using the Stream data constructors to build it), then you have to be mindful of this invariant.

Moreover, I think this invariant makes sense to enforce. Drop is a special operation with somewhat non-obvious safety criteria, so it makes sense that we would try to normalize Drop expressions into a form where it is easier to check whether they are valid or not.

Claim 2: The drop function enforces the Drop invariant

Although reification imposes a tight constraint on what forms Drop can have, the user-facing drop function is more permissive. For instance, it is perfectly fine to call the drop function on a constant stream (i.e., a Const):

Because reification would reject Drop _ (Const _), the drop function ensures that dropping elements from a Const will simply evaluate to another Const. This upholds the Drop invariant (vacuously). drop also has a special case for nested applications of Drop:

As well as another special case for dropping zero elements, which should succeed for all possible streams:

Claim 3: The Drop invariant should put tight bounds on the number of elements being dropped

Since we are already normalizing Drop expressions, we can be fairly strict about the shapes of these expressions. In particular, we know that backends like copilot-c99 translate Drop expressions to array indexes, so if you have an expression like drop k (xs ++ s), then it is likely that copilot-c99 will translate this into an array access at index i. As such, I think it makes sense for reification to ensure that this array index will always be in bounds.

That brings us to this line of code in copilot-language:

I now believe that this check is reasonable, because if xs has length k, then we don't want copilot-c99 to translate this to an array index at index k, as that would be out of bounds. We could check for this on the copilot-c99 side, I suppose, but other backends (e.g., copilot-bluespec) would have the same problem, so I believe it makes sense to enforce this constraint on the copilot-language side.

To summarize: I believe the Drop invariant should require that the number of elements being dropped should be strictly less than the number of elements in the Append. Under this interpretation, the k >= length xs check is reasonable.

Claim 4: The drop function should have a special case for when the number of dropped elements equals the number of Appended elements

If the Drop invariant requires that the number of elements being dropped should be strictly less than the number of elements in the Append, then that raises a question of what to do for things like drop k (xs ++ s), where xs's length is equal to k. The documentation for the drop currently claims that this is permitted, but the stronger Drop invariant that I arrived at in Claim 3 appears to be at odds with this goal.

As I noted in Claim 2, however, these goals aren't at odds after all. This is because the drop function is responsible for enforcing the Drop invariant, so we can uphold the stronger requirements with another special case in drop's implementation:

drop k ( Append xs _ s ) | i == length xs = s

This strips off the outermost Drop if the length equals k, thereby upholding the stronger Drop invariant (again, vacuously). What's more, this is the only change we need to make to copilot-language—no modifications to analysis or reification are required.